// 
// File:   add_vector.h
// Author: cionescu
//
// Created on February 18, 2007, 12:17 AM
//

#ifndef _add_vector_H
#define	_add_vector_H

class add_vector {
  DdManager* manager;
  DdNode* vector;
  DdNode** vars;
  int num_vars;
  
  public:
    
    add_vector(DdManager* _m, DdNode** _v, int _n) 
    : manager(_m), vars(_v), num_vars(_n) {
      vector = DD_Constant(manager, 0);
    }
    
    add_vector(DdManager* _m, add_variables& v) 
    : manager(_m) {
      vars = v.get_raw_vector();
      num_vars = v.get_encoding_size();
      vector = DD_Constant(_m, 0);
    }
    
    void
    set_element(int index, double value) {
      vector = DD_SetVectorElement(manager, vector, vars, num_vars, index, value);
    }
    
    double
    get_element(int index) {
      return DD_GetVectorElement(manager, vector, vars, num_vars, index);
    }
    
    DdNode*
    get_add() {
      return vector;
    }
    
    void
    print() {
      DD_PrintVector(manager, vector, vars, num_vars);
    }
};

#endif	/* _add_vector_H */

